$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$), $f$:($\forall$$x$:$T$. Dec($P$($x$))), $x$:$T$. ($\uparrow$can{-}apply(p{-}filter($f$);$x$)) $\Leftarrow\!\Rightarrow$ $P$($x$)